; [12] **** Yet another theorem-prover ****
; Rewrite rule base theorem-proving programs
;         written by Bob Boyer.

(SETQ BASE 10. IBASE 10.)

(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))

(DEFUN ADD-LEMMA (TERM)
       (COND ((AND (NOT (ATOM TERM))
                   (EQ (CAR TERM)
                       (QUOTE EQUAL))
                   (NOT (ATOM (CADR TERM))))
              (PUTPROP (CAR (CADR TERM))
                       (CONS TERM (GET (CAR (CADR TERM))
                                           (QUOTE LEMMAS)))
                       (QUOTE LEMMAS)))
             (T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
                       TERM))))
(DEFUN ADD-LEMMA-LST (LST)
       (COND ((NULL LST)
              T)
             (T (ADD-LEMMA (CAR LST))
                (ADD-LEMMA-LST (CDR LST)))))
(DEFUN APPLY-SUBST (ALIST TERM)
       (COND ((ATOM TERM)
              (COND ((SETQ TEMP-TEMP (ASSQ TERM ALIST))
                     (CDR TEMP-TEMP))
                    (T TERM)))
             (T (CONS (CAR TERM)
                      (APPLY-SUBST-LST ALIST (CDR TERM))))))
(DEFUN APPLY-SUBST-LST (ALIST LST)
       (COND ((NULL LST)
              NIL)
             (T (CONS (APPLY-SUBST ALIST (CAR LST))
                      (APPLY-SUBST-LST ALIST (CDR LST))))))
(DEFUN FALSEP (X LST)
       (OR (EQUAL X (QUOTE (F)))
           (MEMBER X LST)))
(DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
       (PROGN (SETQ UNIFY-SUBST NIL)
              (ONE-WAY-UNIFY1 TERM1 TERM2)))
(DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
       (COND ((ATOM TERM2)
              (COND ((SETQ TEMP-TEMP (ASSQ TERM2 UNIFY-SUBST))
                     (EQUAL TERM1 (CDR TEMP-TEMP)))
                    (T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
                                               UNIFY-SUBST))
                       T)))
             ((ATOM TERM1)
              NIL)
             ((EQ (CAR TERM1)
                  (CAR TERM2))
              (ONE-WAY-UNIFY1-LST (CDR TERM1)
                                  (CDR TERM2)))
             (T NIL)))
(DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
       (COND ((NULL LST1)
              T)
             ((ONE-WAY-UNIFY1 (CAR LST1)
                              (CAR LST2))
              (ONE-WAY-UNIFY1-LST (CDR LST1)
                                  (CDR LST2)))
             (T NIL)))
(DEFUN REWRITE (TERM)
       (COND ((ATOM TERM)
              TERM)
             (T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
                                           (REWRITE-ARGS (CDR TERM)))
                                     (GET (CAR TERM)
                                              (QUOTE LEMMAS))))))
(DEFUN REWRITE-ARGS (LST)
       (COND ((NULL LST)
              NIL)
             (T (CONS (REWRITE (CAR LST))
                      (REWRITE-ARGS (CDR LST))))))
(DEFUN REWRITE-WITH-LEMMAS (TERM LST)
       (COND ((NULL LST)
              TERM)
             ((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
              (REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
             (T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DEFUN
  SETUP NIL
  (ADD-LEMMA-LST
    (QUOTE ((EQUAL (COMPILE FORM)
                   (REVERSE (CODEGEN (OPTIMIZE FORM)
                                     (NIL))))
            (EQUAL (EQP X Y)
                   (EQUAL (FIX X)
                          (FIX Y)))
            (EQUAL (GREATERP X Y)
                   (LESSP Y X))
            (EQUAL (LESSEQP X Y)
                   (NOT (LESSP Y X)))
            (EQUAL (GREATEREQP X Y)
                   (NOT (LESSP X Y)))
            (EQUAL (BOOLEAN X)
                   (OR (EQUAL X (T))
                       (EQUAL X (F))))
            (EQUAL (IFF X Y)
                   (AND (IMPLIES X Y)
                        (IMPLIES Y X)))
            (EQUAL (EVEN1 X)
                   (IF (ZEROP X)
                       (T)
                       (ODD (SUB1 X))))
            (EQUAL (COUNTPS- L PRED)
                   (COUNTPS-LOOP L PRED (ZERO)))
            (EQUAL (FACT- I)
                   (FACT-LOOP I 1))
            (EQUAL (REVERSE- X)
                   (REVERSE-LOOP X (NIL)))
            (EQUAL (DIVIDES X Y)
                   (ZEROP (REMAINDER Y X)))
            (EQUAL (ASSUME-TRUE VAR ALIST)
                   (CONS (CONS VAR (T))
                         ALIST))
            (EQUAL (ASSUME-FALSE VAR ALIST)
                   (CONS (CONS VAR (F))
                         ALIST))
            (EQUAL (TAUTOLOGY-CHECKER X)
                   (TAUTOLOGYP (NORMALIZE X)
                               (NIL)))
            (EQUAL (FALSIFY X)
                   (FALSIFY1 (NORMALIZE X)
                             (NIL)))
            (EQUAL (PRIME X)
                   (AND (NOT (ZEROP X))
                        (NOT (EQUAL X (ADD1 (ZERO))))
                        (PRIME1 X (SUB1 X))))
            (EQUAL (AND P Q)
                   (IF P (IF Q (T)
                             (F))
                       (F)))
            (EQUAL (OR P Q)
                   (IF P (T)
                       (IF Q (T)
                           (F))
                       (F)))
            (EQUAL (NOT P)
                   (IF P (F)
                       (T)))
            (EQUAL (IMPLIES P Q)
                   (IF P (IF Q (T)
                             (F))
                       (T)))
            (EQUAL (FIX X)
                   (IF (NUMBERP X)
                       X
                       (ZERO)))
            (EQUAL (IF (IF A B C)
                       D E)
                   (IF A (IF B D E)
                       (IF C D E)))
            (EQUAL (ZEROP X)
                   (OR (EQUAL X (ZERO))
                       (NOT (NUMBERP X))))
            (EQUAL (PLUS (PLUS X Y)
                         Z)
                   (PLUS X (PLUS Y Z)))
            (EQUAL (EQUAL (PLUS A B)
                          (ZERO))
                   (AND (ZEROP A)
                        (ZEROP B)))
            (EQUAL (DIFFERENCE X X)
                   (ZERO))
            (EQUAL (EQUAL (PLUS A B)
                          (PLUS A C))
                   (EQUAL (FIX B)
                          (FIX C)))
            (EQUAL (EQUAL (ZERO)
                          (DIFFERENCE X Y))
                   (NOT (LESSP Y X)))
            (EQUAL (EQUAL X (DIFFERENCE X Y))
                   (AND (NUMBERP X)
                        (OR (EQUAL X (ZERO))
                            (ZEROP Y))))
            (EQUAL (MEANING (PLUS-TREE (APPEND X Y))
                            A)
                   (PLUS (MEANING (PLUS-TREE X)
                                  A)
                         (MEANING (PLUS-TREE Y)
                                  A)))
            (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
                            A)
                   (FIX (MEANING X A)))
            (EQUAL (APPEND (APPEND X Y)
                           Z)
                   (APPEND X (APPEND Y Z)))
            (EQUAL (REVERSE (APPEND A B))
                   (APPEND (REVERSE B)
                           (REVERSE A)))
            (EQUAL (TIMES X (PLUS Y Z))
                   (PLUS (TIMES X Y)
                         (TIMES X Z)))
            (EQUAL (TIMES (TIMES X Y)
                          Z)
                   (TIMES X (TIMES Y Z)))
            (EQUAL (EQUAL (TIMES X Y)
                          (ZERO))
                   (OR (ZEROP X)
                       (ZEROP Y)))
            (EQUAL (EXEC (APPEND X Y)
                         PDS ENVRN)
                   (EXEC Y (EXEC X PDS ENVRN)
                         ENVRN))
            (EQUAL (MC-FLATTEN X Y)
                   (APPEND (FLATTEN X)
                           Y))
            (EQUAL (MEMBER X (APPEND A B))
                   (OR (MEMBER X A)
                       (MEMBER X B)))
            (EQUAL (MEMBER X (REVERSE Y))
                   (MEMBER X Y))
            (EQUAL (LENGTH (REVERSE X))
                   (LENGTH X))
            (EQUAL (MEMBER A (INTERSECT B C))
                   (AND (MEMBER A B)
                        (MEMBER A C)))
            (EQUAL (NTH (ZERO)
                        I)
                   (ZERO))
            (EQUAL (EXP I (PLUS J K))
                   (TIMES (EXP I J)
                          (EXP I K)))
            (EQUAL (EXP I (TIMES J K))
                   (EXP (EXP I J)
                        K))
            (EQUAL (REVERSE-LOOP X Y)
                   (APPEND (REVERSE X)
                           Y))
            (EQUAL (REVERSE-LOOP X (NIL))
                   (REVERSE X))
            (EQUAL (COUNT-LIST Z (SORT-LP X Y))
                   (PLUS (COUNT-LIST Z X)
                         (COUNT-LIST Z Y)))
            (EQUAL (EQUAL (APPEND A B)
                          (APPEND A C))
                   (EQUAL B C))
            (EQUAL (PLUS (REMAINDER X Y)
                         (TIMES Y (QUOTIENT X Y)))
                   (FIX X))
            (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
                               BASE)
                   (PLUS (POWER-EVAL L BASE)
                         I))
            (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
                               BASE)
                   (PLUS I (PLUS (POWER-EVAL X BASE)
                                 (POWER-EVAL Y BASE))))
            (EQUAL (REMAINDER Y 1)
                   (ZERO))
            (EQUAL (LESSP (REMAINDER X Y)
                          Y)
                   (NOT (ZEROP Y)))
            (EQUAL (REMAINDER X X)
                   (ZERO))
            (EQUAL (LESSP (QUOTIENT I J)
                          I)
                   (AND (NOT (ZEROP I))
                        (OR (ZEROP J)
                            (NOT (EQUAL J 1)))))
            (EQUAL (LESSP (REMAINDER X Y)
                          X)
                   (AND (NOT (ZEROP Y))
                        (NOT (ZEROP X))
                        (NOT (LESSP X Y))))
            (EQUAL (POWER-EVAL (POWER-REP I BASE)
                               BASE)
                   (FIX I))
            (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
                                         (POWER-REP J BASE)
                                         (ZERO)
                                         BASE)
                               BASE)
                   (PLUS I J))
            (EQUAL (GCD X Y)
                   (GCD Y X))
            (EQUAL (NTH (APPEND A B)
                        I)
                   (APPEND (NTH A I)
                           (NTH B (DIFFERENCE I (LENGTH A)))))
            (EQUAL (DIFFERENCE (PLUS X Y)
                               X)
                   (FIX Y))
            (EQUAL (DIFFERENCE (PLUS Y X)
                               X)
                   (FIX Y))
            (EQUAL (DIFFERENCE (PLUS X Y)
                               (PLUS X Z))
                   (DIFFERENCE Y Z))
            (EQUAL (TIMES X (DIFFERENCE C W))
                   (DIFFERENCE (TIMES C X)
                               (TIMES W X)))
            (EQUAL (REMAINDER (TIMES X Z)
                              Z)
                   (ZERO))
            (EQUAL (DIFFERENCE (PLUS B (PLUS A C))
                               A)
                   (PLUS B C))
            (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
                               Z)
                   (ADD1 Y))
            (EQUAL (LESSP (PLUS X Y)
                          (PLUS X Z))
                   (LESSP Y Z))
            (EQUAL (LESSP (TIMES X Z)
                          (TIMES Y Z))
                   (AND (NOT (ZEROP Z))
                        (LESSP X Y)))
            (EQUAL (LESSP Y (PLUS X Y))
                   (NOT (ZEROP X)))
            (EQUAL (GCD (TIMES X Z)
                        (TIMES Y Z))
                   (TIMES Z (GCD X Y)))
            (EQUAL (VALUE (NORMALIZE X)
                          A)
                   (VALUE X A))
            (EQUAL (EQUAL (FLATTEN X)
                          (CONS Y (NIL)))
                   (AND (NLISTP X)
                        (EQUAL X Y)))
            (EQUAL (LISTP (GOPHER X))
                   (LISTP X))
            (EQUAL (SAMEFRINGE X Y)
                   (EQUAL (FLATTEN X)
                          (FLATTEN Y)))
            (EQUAL (EQUAL (GREATEST-FACTOR X Y)
                          (ZERO))
                   (AND (OR (ZEROP Y)
                            (EQUAL Y 1))
                        (EQUAL X (ZERO))))
            (EQUAL (EQUAL (GREATEST-FACTOR X Y)
                          1)
                   (EQUAL X 1))
            (EQUAL (NUMBERP (GREATEST-FACTOR X Y))
                   (NOT (AND (OR (ZEROP Y)
                                 (EQUAL Y 1))
                             (NOT (NUMBERP X)))))
            (EQUAL (TIMES-LIST (APPEND X Y))
                   (TIMES (TIMES-LIST X)
                          (TIMES-LIST Y)))
            (EQUAL (PRIME-LIST (APPEND X Y))
                   (AND (PRIME-LIST X)
                        (PRIME-LIST Y)))
            (EQUAL (EQUAL Z (TIMES W Z))
                   (AND (NUMBERP Z)
                        (OR (EQUAL Z (ZERO))
                            (EQUAL W 1))))
            (EQUAL (GREATEREQPR X Y)
                   (NOT (LESSP X Y)))
            (EQUAL (EQUAL X (TIMES X Y))
                   (OR (EQUAL X (ZERO))
                       (AND (NUMBERP X)
                            (EQUAL Y 1))))
            (EQUAL (REMAINDER (TIMES Y X)
                              Y)
                   (ZERO))
            (EQUAL (EQUAL (TIMES A B)
                          1)
                   (AND (NOT (EQUAL A (ZERO)))
                        (NOT (EQUAL B (ZERO)))
                        (NUMBERP A)
                        (NUMBERP B)
                        (EQUAL (SUB1 A)
                               (ZERO))
                        (EQUAL (SUB1 B)
                               (ZERO))))
            (EQUAL (LESSP (LENGTH (DELETE X L))
                          (LENGTH L))
                   (MEMBER X L))
            (EQUAL (SORT2 (DELETE X L))
                   (DELETE X (SORT2 L)))
            (EQUAL (DSORT X)
                   (SORT2 X))
            (EQUAL (LENGTH (CONS X1
                                 (CONS X2
                                       (CONS X3 (CONS X4
                                                      (CONS X5
                                                            (CONS X6 X7)))))))
                   (PLUS 6 (LENGTH X7)))
            (EQUAL (DIFFERENCE (ADD1 (ADD1 X))
                               2)
                   (FIX X))
            (EQUAL (QUOTIENT (PLUS X (PLUS X Y))
                             2)
                   (PLUS X (QUOTIENT Y 2)))
            (EQUAL (SIGMA (ZERO)
                          I)
                   (QUOTIENT (TIMES I (ADD1 I))
                             2))
            (EQUAL (PLUS X (ADD1 Y))
                   (IF (NUMBERP Y)
                       (ADD1 (PLUS X Y))
                       (ADD1 X)))
            (EQUAL (EQUAL (DIFFERENCE X Y)
                          (DIFFERENCE Z Y))
                   (IF (LESSP X Y)
                       (NOT (LESSP Y Z))
                       (IF (LESSP Z Y)
                           (NOT (LESSP Y X))
                           (EQUAL (FIX X)
                                  (FIX Z)))))
            (EQUAL (MEANING (PLUS-TREE (DELETE X Y))
                            A)
                   (IF (MEMBER X Y)
                       (DIFFERENCE (MEANING (PLUS-TREE Y)
                                            A)
                                   (MEANING X A))
                       (MEANING (PLUS-TREE Y)
                                A)))
            (EQUAL (TIMES X (ADD1 Y))
                   (IF (NUMBERP Y)
                       (PLUS X (TIMES X Y))
                       (FIX X)))
            (EQUAL (NTH (NIL)
                        I)
                   (IF (ZEROP I)
                       (NIL)
                       (ZERO)))
            (EQUAL (LAST (APPEND A B))
                   (IF (LISTP B)
                       (LAST B)
                       (IF (LISTP A)
                           (CONS (CAR (LAST A))
                                 B)
                           B)))
            (EQUAL (EQUAL (LESSP X Y)
                          Z)
                   (IF (LESSP X Y)
                       (EQUAL T Z)
                       (EQUAL F Z)))
            (EQUAL (ASSIGNMENT X (APPEND A B))
                   (IF (ASSIGNEDP X A)
                       (ASSIGNMENT X A)
                       (ASSIGNMENT X B)))
            (EQUAL (CAR (GOPHER X))
                   (IF (LISTP X)
                       (CAR (FLATTEN X))
                       (ZERO)))
            (EQUAL (FLATTEN (CDR (GOPHER X)))
                   (IF (LISTP X)
                       (CDR (FLATTEN X))
                       (CONS (ZERO)
                             (NIL))))
            (EQUAL (QUOTIENT (TIMES Y X)
                             Y)
                   (IF (ZEROP Y)
                       (ZERO)
                       (FIX X)))
            (EQUAL (GET J (SET I VAL MEM))
                   (IF (EQP J I)
                       VAL
                       (GET J MEM)))))))
(DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
       (COND ((TRUEP X TRUE-LST)
              T)
             ((FALSEP X FALSE-LST)
              NIL)
             ((ATOM X)
              NIL)
             ((EQ (CAR X)
                  (QUOTE IF))
              (COND ((TRUEP (CADR X)
                            TRUE-LST)
                     (TAUTOLOGYP (CADDR X)
                                 TRUE-LST FALSE-LST))
                    ((FALSEP (CADR X)
                             FALSE-LST)
                     (TAUTOLOGYP (CADDDR X)
                                 TRUE-LST FALSE-LST))
                    (T (AND (TAUTOLOGYP (CADDR X)
                                        (CONS (CADR X)
                                              TRUE-LST)
                                        FALSE-LST)
                            (TAUTOLOGYP (CADDDR X)
                                        TRUE-LST
                                        (CONS (CADR X)
                                              FALSE-LST))))))
             (T NIL)))
(DEFUN TAUTP (X)
       (TAUTOLOGYP (REWRITE X)
                   NIL NIL))
(DEFUN TEST NIL
       (PROG (ANS TERM)
             (SETQ TERM
                   (APPLY-SUBST
                     (QUOTE ((X F (PLUS (PLUS A B)
                                        (PLUS C (ZERO))))
                             (Y F (TIMES (TIMES A B)
                                         (PLUS C D)))
                             (Z F (REVERSE (APPEND (APPEND A B)
                                                   (NIL))))
                             (U EQUAL (PLUS A B)
                                (DIFFERENCE X Y))
                             (W LESSP (REMAINDER A B)
                                (MEMBER A (LENGTH B)))))
                     (QUOTE (IMPLIES (AND (IMPLIES X Y)
                                          (AND (IMPLIES Y Z)
                                               (AND (IMPLIES Z U)
                                                    (IMPLIES U W))))
                                     (IMPLIES X W)))))
             (SETQ ANS (TAUTP TERM)) ))

(DEFUN TRANS-OF-IMPLIES (N)
       (LIST (QUOTE IMPLIES)
             (TRANS-OF-IMPLIES1 N)
             (LIST (QUOTE IMPLIES)
                   0 N)))
(DEFUN TRANS-OF-IMPLIES1 (N)
       (COND ((EQUAL N 1)
              (LIST (QUOTE IMPLIES)
                    0 1))
             (T (LIST (QUOTE AND)
                      (LIST (QUOTE IMPLIES)
                            (SUB1 N)
                            N)
                      (TRANS-OF-IMPLIES1 (SUB1 N))))))
(DEFUN TRUEP (X LST)
       (OR (EQUAL X (QUOTE (T)))
           (MEMBER X LST)))

; Initialization

(SETUP)

; Confirm that (TEST) must return T.

; [12-1:] Measure the following execution time.

(DEFMACRO BENCHMARK (N &REST BODY)
  `(LET (TIME1 TIME2 TIME3 GC RUN)
     (PRINT ',BODY)
     (GC)
     (SSTATUS GCTIME 0)
     (SETQ TIME1 (RUNTIME))
     (DO ((I 1 (1+ I)))
	 ((> I ,N))
       ,@BODY )
     (SETQ TIME2 (RUNTIME))
     (DO ((I 1 (1+ I))) ((> I ,N)))
     (SETQ TIME3 (RUNTIME))
     (SETQ GC (STATUS GCTIME))
     (SETQ RUN (DIFFERENCE (PLUS TIME2 TIME2) TIME1 TIME3))
     (TERPRI)
     (PRINC "Total = ")
     (PRINC RUN)
     (PRINC "us,  Runtime = ")
     (PRINC (DIFFERENCE RUN GC))
     (PRINC "us, GC = ")
     (PRINC GC)
     (PRINC "us, for ")
     (PRINC ,N)
     (PRINC " iterations.")
     (TERPRI)
     ))

(DEFUN BENCH121 (ITER) (BENCHMARK ITER (TEST)))

; If macro is not avaiable, use instead the followings:

'("*** Please this line and the last line. ***"

(DEFUN BENCH121 (ITER)
  (PROG (TIME1 TIME2 TIME3 GC RUN N)
        (GC)
	(SSTATUS GCTIME 0)
	(SETQ TIME1 (RUNTIME))
	(SETQ N ITER)
   L1   (TEST)
	(COND ((GREATERP (SETQ N (SUB1 N)) 0) (GO L1)))
	(SETQ TIME2 (RUNTIME))
	(SETQ N ITER)
   L2   (COND ((GREATERP (SETQ N (SUB1 N)) 0) (GO L2)))
	(SETQ TIME3 (RUNTIME))
	(SETQ GC (STATUS GCTIME))
	(SETQ RUN (DIFFERENCE (PLUS TIME2 TIME2) TIME1 TIME3))
	(TERPRI)
	(PRINC "Total = ")
	(PRINC RUN)
	(PRINC "us,  Runtime = ")
	(PRINC (DIFFERENCE RUN GC))
	(PRINC "us, GC = ")
	(PRINC GC)
	(PRINC "us, for ")
	(PRINC ITER)
	(PRINC " iterations.")
	(TERPRI)
        ))

"*** Please kill this line. ***" )

; Now measure the benchmark.
; (BENCH121 1)

; ******** That's all ********